mere propositions
mere propositions(単命題?)
ChatGPTによる訳は単命題
ホモトピー型理論
(-1)-truncated objectとか、h-propositionsと呼ばれる
(-1)-groupoid
、(-1)-truncated objectsに対応する
定義
型
$ P
が単命題(mere proposition)とは任意の
$ x,y: P
について
$ x = y
$ P : \mathscr{U}
$ \mathrm{isProp}(P) :\equiv \prod_{x,y:P} (x = y)
参考
mere proposition in nLab
3.3 Mere propositions
関連
型宇宙
propositions as types
局所デカルト閉圏
メモ
『Homotopy Type Theory Univalent Foundations of Mathematics』 目次
P111 3.3 Mere propositions
#Homotopy_Type_Theory(HoTT)
#数学